\chapter{Computabilidade}


\subsection{Definicoes:}
\begin{enumerate}
\item A e nao trivial se: 
\begin{displaymath}
A \neq \emptyset \wedge A \neq \varLambda
\end{displaymath}

\item A e fechado sobre igualdade se A e nao trivial, e nao 'e recursivo:

\item A e B sao recursivamente separaveis se, A e B sao fechados sobre igualdade e conjuntos vazios de $\Lambda$.

\end{enumerate}


\subsection{Teorema de Scott}
\begin{enumerate}
\item Sejam A e B, subconjuntos nao vazios de $\varLambda$ fechado sobre igualdade, A e B nao sao recursivamentes separaveis.
\item Seja A um subconjunto nao trivial de $\varLambda$ fechado sobre igualdade, A nao e recursivo. 
\end{enumerate}

Teorema para mostrar se um termo $ M \in \varLambda $, possui uma $ \beta-nf$, 'e equivalente ao problema da parada para as maquinas de Turing, portanto sao indecidiveis.

%\subsection{Teorema $ \{ M|M $ possui uma nf $ \} $ e um conjunto recursivamente enumeravel que nao e recursivo}

Para que o conjunto $ \{ M|M $ possui uma nf $ \} $ seja recursivamente enumerado o M tem que possuir uma nf $ \leftrightarrow \exists N.N $
 e $\lambda \vdash M=N $, um procediemnto com uma sequencias de formas normais testa a igualdade de M, este procedimento porem so para se e somente se M for igual a uma forma normal, como as formas normais existem em infinidade, o procedimento corre o risco de nao parar, uma vez que o M for nao trivial, pelo teorema de Scott tem-se que o conjunto M sendo nao trivial e fechado sobre igualdade ele nao pode ser recursivo, concluindo que o problema e indecidivel.

\subsection{Funcoes computaveis}

Para se escrever um programa lambda e necessario um conjunto de expressoes lambda.
Geralmente e o simbolo lambda seguido de variaveis $($também chamadas parametros$)$, 
limitando cada variavel vem um ponto $(.)$, logo depois vem o corpo da funcao $($costuma se usar operadores prefixados$)$.

ex:
\begin{displaymath}
\lambda x . (+ x 1)
x=5
\lambda x,(+ x 1).5
\end{displaymath}


Na sua forma mais pura o calculo lambda nao suporta o operador de soma. Porem existem extensoes que as suportem, assim como constantes,
funcoes booleanas e as demais funcoes aritimeticas basica.

\subsection{Operacoes booleanas} 

\textbf{True e False}

True recebe dois argumentos e responde necessariamente o primeiro, ja o false retorna o segundo.

Ex:

True = $\lambda$ xy.x
False =$\lambda$ xy.y

\textbf{And}

Representada pelo simbolo $\wedge$, funcao de dois ou mais argumentos.

Ex:
\begin{displaymath}
\wedge \equiv \lambda xy.x ( \lambda  uv.v) \equiv \lambda xy.xyF
\end{displaymath}


Nesta função And o retorno foi false, por que para que o resultado se verdadeiro e necessário que ambas as funcoes $\lambda$ respondam o primeiro argumento.

\subsection{Teste Condicional}

E possivel definir operacao de teste condicional com a propriedade: IF bvw reduz pra v quando b e true e para w quando b e false.
